equiv_rel_self_fun_com 12,41
This lemma is useful for quickly proving functionality
lemmas for equivalence relations.

origin